The Runtime Complexity (full) of the given CpxTRS could be proven to be BOUNDS(n^1, INF).

(0) Obligation:

Runtime Complexity TRS:
The TRS R consists of the following rules:

if(true, t, e) → t
if(false, t, e) → e
member(x, nil) → false
member(x, cons(y, ys)) → if(eq(x, y), true, member(x, ys))
eq(nil, nil) → true
eq(O(x), 0(y)) → eq(x, y)
eq(0(x), 1(y)) → false
eq(1(x), 0(y)) → false
eq(1(x), 1(y)) → eq(x, y)
negate(0(x)) → 1(x)
negate(1(x)) → 0(x)
choice(cons(x, xs)) → x
choice(cons(x, xs)) → choice(xs)
guess(nil) → nil
guess(cons(clause, cnf)) → cons(choice(clause), guess(cnf))
verify(nil) → true
verify(cons(l, ls)) → if(member(negate(l), ls), false, verify(ls))
sat(cnf) → satck(cnf, guess(cnf))
satck(cnf, assign) → if(verify(assign), assign, unsat)

Rewrite Strategy: FULL

(1) CpxTrsToCpxRelTrsProof (BOTH BOUNDS(ID, ID) transformation)

Transformed TRS to relative TRS where S is empty.

(2) Obligation:

Runtime Complexity Relative TRS:
The TRS R consists of the following rules:

if(true, t, e) → t
if(false, t, e) → e
member(x, nil) → false
member(x, cons(y, ys)) → if(eq(x, y), true, member(x, ys))
eq(nil, nil) → true
eq(O(x), 0(y)) → eq(x, y)
eq(0(x), 1(y)) → false
eq(1(x), 0(y)) → false
eq(1(x), 1(y)) → eq(x, y)
negate(0(x)) → 1(x)
negate(1(x)) → 0(x)
choice(cons(x, xs)) → x
choice(cons(x, xs)) → choice(xs)
guess(nil) → nil
guess(cons(clause, cnf)) → cons(choice(clause), guess(cnf))
verify(nil) → true
verify(cons(l, ls)) → if(member(negate(l), ls), false, verify(ls))
sat(cnf) → satck(cnf, guess(cnf))
satck(cnf, assign) → if(verify(assign), assign, unsat)

S is empty.
Rewrite Strategy: FULL

(3) SlicingProof (LOWER BOUND(ID) transformation)

Sliced the following arguments:
satck/0

(4) Obligation:

Runtime Complexity Relative TRS:
The TRS R consists of the following rules:

if(true, t, e) → t
if(false, t, e) → e
member(x, nil) → false
member(x, cons(y, ys)) → if(eq(x, y), true, member(x, ys))
eq(nil, nil) → true
eq(O(x), 0(y)) → eq(x, y)
eq(0(x), 1(y)) → false
eq(1(x), 0(y)) → false
eq(1(x), 1(y)) → eq(x, y)
negate(0(x)) → 1(x)
negate(1(x)) → 0(x)
choice(cons(x, xs)) → x
choice(cons(x, xs)) → choice(xs)
guess(nil) → nil
guess(cons(clause, cnf)) → cons(choice(clause), guess(cnf))
verify(nil) → true
verify(cons(l, ls)) → if(member(negate(l), ls), false, verify(ls))
sat(cnf) → satck(guess(cnf))
satck(assign) → if(verify(assign), assign, unsat)

S is empty.
Rewrite Strategy: FULL

(5) DecreasingLoopProof (EQUIVALENT transformation)

The following loop(s) give(s) rise to the lower bound Ω(n¹):
The rewrite sequence
member(x, cons(y, ys)) →⁺ if(eq(x, y), true, member(x, ys))
gives rise to a decreasing loop by considering the right hand sides subterm at position [2].
The pumping substitution is [ys / cons(y, ys)].
The result substitution is [ ].

(6) BOUNDS(n^1, INF)